Inference at * 
Iof proof for Lemma can-apply-compose-iff:


  A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)), x:A.
  (can-apply(f o g  ;x))  ((can-apply(g;x)) & (can-apply(f;do-apply(g;x)))) 

latex

 by ((MaAuto) 
CollapseTHEN (AllHyps (\h. ((FLemma `can-apply-compose` [h]) 
CollapseTHEN (Auto))
Co ))) 

latex

Co1: 

Co1: 1. A : Type
Co1: 2. B : Type
Co1: 3. C : Type
Co1: 4. g : A(B + Top)
Co1: 5. f : B(C + Top)
Co1: 6. x : A
Co1: 7. can-apply(g;x)
Co1: 8. can-apply(f;do-apply(g;x))
Co1:   can-apply(f o g  ;x)
Co.

Definitions	Top, P  Q, P  Q, x:A  B(x), A c B, , b, if b then t else f fi , True, case b of inl(x) => s(x) | inr(y) => t(y), f(a), do-apply(f;x), tt, ff, left + right, Unit, , x:AB(x), Type, t  T, x:A. B(x), P  Q, {T}, P & Q
Lemmas	do-apply wf, btrue wf, bfalse wf, can-apply-compose